<html>
<head><meta charset="utf-8"><title>Gauging sanity of project idea · t-lang/wg-unsafe-code-guidelines · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/index.html">t-lang/wg-unsafe-code-guidelines</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging.20sanity.20of.20project.20idea.html">Gauging sanity of project idea</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="187780612"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging%20sanity%20of%20project%20idea/near/187780612" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging.20sanity.20of.20project.20idea.html#187780612">(Feb 10 2020 at 00:20)</a>:</h4>
<p>Project idea: given a piece of unsafe code, make a list of all the invariants you need to uphold, so you can be sure you don't forget to check an invariant you need to uphold when looking at unsafe code. Inspired by The Checklist Manifesto.<br>
e.g. if there is a raw pointer dereference =&gt; non-null, alignment, aliasing, provenance, in bounds, target is initialized (and I'm probably forgetting something)<br>
Any thoughts on whether this is feasible or practical?</p>



<a name="187839864"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging%20sanity%20of%20project%20idea/near/187839864" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging.20sanity.20of.20project.20idea.html#187839864">(Feb 10 2020 at 17:57)</a>:</h4>
<p>hm... sounds like an interesting experiment. we have some long-term plans to do that in a formal way (so, it would list all the coq proof obligations you have to show), but doing something that normal people can read would probably be more widely applicable :D</p>



<a name="188223215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging%20sanity%20of%20project%20idea/near/188223215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging.20sanity.20of.20project.20idea.html#188223215">(Feb 14 2020 at 16:43)</a>:</h4>
<p>Related to something I've always wanted:</p>
<p>I've wanted wanted to be able to informally write the "things one must prove" in the form of prolog-like predicates. e.g., <code>NotNull(x)</code>, where <code>x</code> is the name of a parameter or something, and then have a tool that lints that -- on the relevant unsafe block around a call <code>foo(y)</code> -- I have written something like <code>// assert NotNull(y)</code>. </p>
<p>The idea here is:</p>
<ul>
<li>I am saying I thought about this condition and believe it holds</li>
<li>If I add a new condition to <code>foo</code>, like <code>Aligned(x)</code>, then I'll start to get lint errors at every call site until I added <code>// assert Aligned(y)</code> to state that I believe it holds.</li>
</ul>
<p>The whole idea is just to track "what are the things I think I thought about".</p>



<a name="188319262"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging%20sanity%20of%20project%20idea/near/188319262" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Elichai Turkel <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging.20sanity.20of.20project.20idea.html#188319262">(Feb 16 2020 at 09:22)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> This sounds pretty cool, because for me the hardest part is revisiting some unsafe code and modifying it but forgetting some weird invariant I added a while ago</p>



<a name="188332186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging%20sanity%20of%20project%20idea/near/188332186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging.20sanity.20of.20project.20idea.html#188332186">(Feb 16 2020 at 17:19)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> yeah that sounds like an awesome tool indeed :D</p>



<a name="188407598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging%20sanity%20of%20project%20idea/near/188407598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Gauging.20sanity.20of.20project.20idea.html#188407598">(Feb 17 2020 at 21:25)</a>:</h4>
<p>maybe some of these use-cases could be modeled with <code>mirai</code> since it seems to handle <em>some</em> form of pre/post conditions/invariants contracts</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>